| Definitions | outl(x), t.2, tag(k), rcv(l,tg), tag(e), P   Q, P  Q, {T}, SQType(T), tt,  , suptype(S; T), S  T, Y, ff, reduce(f;k;as), t.1, deq-member(eq;x;L), x  dom(f), Top, if b then t else f fi ,  , f(x)?z,   x. t(x), t T, R-da(R;i), Valtype(da;k),  e@i. P(e), R-state(R;i), State(ds), state@i, P & Q, R ||- es.P(es), P Q, x:A. B(x), False,  b, Knd, @i(x:T), R-Feasible(R),  x:A. B(x), A c B, @i: only members of L read x, @i:k sends only on links in L, @i: k affects only L, @i Precondition for a:Outcome(p) is P:State(ds)   , sends k(v:T) on l:tagged(g,State(ds),v):dt, @i events of kind k change continuous x to f State(ds) (val:T), @i events of kind k change x to f State(ds) (val:T), only events in L send on l with tg, @i only events in L change x : T, @i continuous x initially v:T, @i x initially v:T, True, Consistent(R;es), x(s), , Unit, Realizer, locl(a), Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), a = b, Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, a = b, Rnone(),  |
| Lemmas | lnk-decl-dom-not, Knd sq, fpf-single-dom, es-kind-rcv, assert-eq-lnk, eq lnk wf, lnk-decl-cap2, R-da wf, decidable equal Id, es-initially wf, subtype rel dep function iff, subtype rel self, R-state wf, subtype rel dep function, es realizer wf, Rrframe wf, Rbframe wf, Raframe wf, Rpre wf, locl wf, p-outcome wf, Rsends wf, lnk-decl wf, fpf-join wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-single wf, fpf-join-cap-sq, lsrc wf, Reffect wf, es-kind wf, fpf-single wf3, ma-valtype wf, assert-eq-knd, eq knd wf, Kind-deq wf, fpf-empty wf, fpf-cap wf, Rsframe wf, Rframe wf, Rinit wf, ifthenelse wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, Id sq, id-deq wf, fpf-cap-single, assert-eq-id, eqtt to assert, assert wf, iff transitivity, eq id wf, Rnone wf, R-Feasible wf, event system wf, R-consistent wf, es-E wf, es-loc wf, es-valtype wf, top wf, es-vartype wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf |